🤖 Kimi Code Review

This PR contains only documentation changes to README.md (lines 135–138). No consensus-critical code, cryptographic logic, or Rust source files are modified.

Review:

• Link correctness: The change appropriately shifts the reference from the tracking Issue 272 to the implementation PR 269. Verify that Issue 272 is indeed superseded by PR 269 or should be closed as completed.
• Markdown structure: The new ### Experimental features subsection assumes a parent ## header exists above line 132. Ensure this heading level matches the document hierarchy (likely under "Features" or "Roadmap").
• Formatting: The bullet point removal leaves a clean list termination. The new paragraph formatting is consistent.

No action required. This documentation update correctly reflects the status migration from planned feature to experimental proof-of-concept.

Automated review by Kimi (Moonshot AI) · kimi-k2.5 · custom prompt

🤖 Codex Code Review

No findings.

The diff only updates documentation in README.md, adding an Experimental features section and a link to PR 269. There are no changes to fork choice, attestation handling, justification/finalization, STF code, XMSS verification, SSZ logic, or any Rust code path, so I don’t see correctness, security, performance, or memory-safety concerns in this PR.

Residual note: since this is README-only, the main risk is documentation drift if PR 269’s status or scope changes later.

Automated review by OpenAI Codex · gpt-5.4 · custom prompt

Greptile Summary

This PR adds a new "Experimental features" subsection to README.md under the "Incoming features" section, briefly documenting a Lean4 proof-of-concept formalization of part of the state transition function and linking to PR #269.

Confidence Score: 5/5

Documentation-only change; safe to merge.

Single-sentence documentation addition with no code changes. No logic, security, or correctness concerns.

No files require special attention.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[README.md - Incoming Features] --> B[Add support for pq-devnet-5]
    A --> C[RPC endpoints for chain data]
    A --> D[ZK proving of STF]
    A --> E[Experimental Features - NEW]
    E --> F[Lean4 formalization of STF\nPR #269 - proof-of-concept]

_{Reviews (1): Last reviewed commit: "docs: add experimental features section ..." | Re-trigger Greptile}

🤖 Claude Code Review

Here is the review for PR 300:

PR Review: docs: add experimental features section to readme

Author: Tomás Grüner
Changes: +4 / -1 in README.md

Overview

This PR adds an "Experimental features" subsection to the README's roadmap area, documenting an ongoing Lean4 formalization proof-of-concept for part of the state transition function (STF). It also removes the trailing entry from the existing "Future features" list (Formal verification of the STF — issue 272).

Analysis

Content accuracy

• The removed item (issue 272) was about formal verification of the STF. The new text references PR 269 as a proof-of-concept formalization in Lean4. These appear to be related but distinct: the issue tracks the goal, while the PR tracks one concrete step toward it. Removing the issue link from the roadmap may cause readers to think formal verification is no longer a goal — consider whether the issue 272 link should be retained alongside or instead of just referencing PR 269.

Completeness of the new section

• The new ### Experimental features section contains only a single sentence referencing one PR. If "Experimental features" is intended to be an ongoing category (like "Future features" above it), a brief note on what "experimental" means in this context (e.g., not production-ready, may be abandoned) would help set reader expectations.
• Linking to a PR rather than an issue or dedicated doc is slightly fragile — PRs can be merged, closed, or superseded. Once PR 269 merges, this line will be inaccurate. Consider whether this should reference the issue tracker or a doc instead.

Formatting

• The diff replaces the last bullet point with a blank line + new heading + prose. The blank line after the previous list item is correct Markdown. No formatting issues.
• The PR reference uses [#269](...) which GitHub will render as a hyperlink with the label "feat: formalize slot_is_justifiable_after in Lean4 #269" — that's fine within Markdown prose (it's not bare #269 that would auto-link as an issue).

Summary

This is a small, low-risk docs-only change. The main concern worth addressing before merging:

1. The removal of the formal verification issue 272 from the roadmap list conflates "we have a PoC in a PR" with "this is no longer a future goal." If the issue is still open and the goal is still alive, it's worth keeping the issue 272 reference somewhere (perhaps as a sub-bullet under the new section, or restored in the future list).
2. Linking to an open PR as the canonical reference for a feature category is fragile — once the PR state changes, the section becomes misleading.

Otherwise, the change is clean and the intent is clear.

Automated review by Claude (Anthropic) · sonnet · custom prompt